\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it es}$:event\_system\{i:l\}, $l$:IdLnk.
\-\\[0ex](source($l$) = $i$) $\Rightarrow$ (ecl{-}mng{-}sends\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $A$; $l$; ${\it snd}$) $\in$ prop\{i:l\})
\end{tabbing}